Issue3002.agda:19,9-13
(λ ()) x != f x of type ⊥
when checking that the expression refl has type
(suc zero ≤? zero) ≡ f
